package ch.epfl.lara.matcheck;

object Timer {

  private var parsing_time: Long = 0l
  private var domain_time: Long = 0l
  private var matcheck_time: Long = 0l

  private var prove_domain_time: Long = 0l
  private var prove_pm_time: Long = 0l
  
  
  private var total_time: Long = 0l
  private var spec_time: Long = 0l
  
  private var time_zero: Long = 0l
  private var time_spec_zero: Long = 0l
  private var time_domain_zero: Long = 0l
  private var time_matcheck_zero: Long = 0l
  
  def start() {
    time_zero = now
  }
  
  def finishedParsing() {
    parsing_time = now - time_zero
    time_zero = now
    time_matcheck_zero = time_zero
  }
  
  
  /** -----------------------------*/
    
  def startSpecVerification() {
    time_spec_zero = now
  }
  
  /** Domains */
  def startDomainVerification() {
    time_domain_zero = now
  }
  
  def startProvingDomain() {
    domain_time = now
  }
  
  def finishedProvingDomain() {
    prove_domain_time = prove_domain_time + (now - domain_time)
  }
  
  def finishedDomainVerification() {
    domain_time = now - (time_domain_zero + prove_domain_time)
  }
  
  private var time_postcondition_zero: Long = 0
  private var postcondition_time: Long = 0
  private var prove_postcondition_time: Long = 0
  
  /** Postconditions */
  def startPostconditionVerification() {
    time_postcondition_zero = now
  }
  
  def startProvingPostcondition() {
    postcondition_time = now
  }
  
  def finishedProvingPostcondition() {
    prove_postcondition_time = prove_postcondition_time + (now - postcondition_time)
  }
  
  def finishedPostconditionVerification() {
    postcondition_time = now - (time_postcondition_zero + prove_postcondition_time)
  }
  
    
  def finishedSpecVerification() {
    spec_time = now - time_spec_zero
    time_matcheck_zero = time_matcheck_zero + spec_time 
  }
  
  /** -----------------------------*/
    
    
  def startPmProver() {
    matcheck_time = now 
  }
  
  def finishedPmProver() {
    prove_pm_time = prove_pm_time + (now  - matcheck_time)
  }
  
  def stop() {
    matcheck_time = (now - time_matcheck_zero - prove_pm_time)
    total_time = parsing_time + prove_pm_time + matcheck_time + spec_time
  }
  
  
  
  private def now = System.currentTimeMillis()
  
  private def millisec2sec(t: Long): Float = t / 1000f
  
  def verbose() {
    Report.verbose("====================================================")
    Report.verbose("=================== Performances ===================")
    Report.verbose("====================================================\n")
                          Report.println("\ntime elpsed for parsing the source file : "+ millisec2sec(parsing_time) +" sec")
    if(!Config.NOSPEC &&
       !Config.NOCHECKS){ Report.println("* time elapsed in the DOMAIN formulae generation : "+ millisec2sec(domain_time) +" sec")
                          Report.println("time elapsed in the proving the generated domain's formulae : "+ millisec2sec(prove_domain_time) +" sec") 
                          Report.println("* time elapsed in the SPEC formulae generation : "+ millisec2sec(postcondition_time) +" sec")
                          Report.println("time elapsed in the proving the generated spec's formulae : "+ millisec2sec(prove_postcondition_time) +" sec")}
                        
    if(!Config.NOCHECKS){ Report.println("* time elapsed in the PATTERN MATCHING formulae generation : "+ millisec2sec(matcheck_time) +" sec")
                          Report.println("time elapsed in the proving the generated pattern matching formulae : "+ millisec2sec(prove_pm_time) +" sec") }
    if(!Config.NOSPEC &&
       !Config.NOCHECKS)  Report.println("> total time elapsed for proving specification : "+ millisec2sec(spec_time)  +" sec" )
    if(!Config.NOCHECKS)  Report.println("> total time elapsed for proving pattern matching : "+ millisec2sec(prove_pm_time + matcheck_time)  +" sec" ) 
                          Report.println("> total time elapsed : "+ millisec2sec(total_time)  +" seconds\n" )
  }
}
